es:ES, l:IdLnk, tg:Id, e:E. ((e  es-in-port(es;l;tg)))  (kind(e) = rcv(l,tg)  Knd) 

latex

Definitions	a = b, kind(e), rcv(l,tg), E, Id, IdLnk, ES, es-in-port(es;l;tg), e  X, can-apply(f;x), left + right, Unit, b, <a, b>, , isl(x), True, x:A  B(x), x:AB(x), Type, x:A. B(x), ff, b, P  Q, P & Q, P  Q, A, P  Q, False, , s = t, t  T, Knd
Lemmas	Knd wf, false wf, assert wf, assert-eq-knd, not functionality wrt iff, true wf, bool wf, rcv wf, es-kind wf, eq knd wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, IdLnk wf, Id wf, es-E wf